\begin{tabbing}
effect\_p(${\it es}$; $i$; ${\it ds}$; $k$; $T$; $x$; $f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))\+
\\[0ex]$\wedge$ subtype\_rel(es{-}kindtype(${\it es}$; $i$; $k$); $T$))
\\[0ex]c$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = $k$)
\\[0ex]$\Rightarrow$ \=(subtype\_rel(es{-}valtype(${\it es}$; $e$); $T$)\+
\\[0ex]c$\wedge$ (es\_state\_after(${\it es}$; $e$)($x$) = $f$(es{-}state{-}when(${\it es}$; $e$),es{-}val(${\it es}$; $e$)))))
\-\\[0ex])
\-\-
\end{tabbing}